| 翻訳と辞書 |
| Hindley–Milner type system ： ウィキペディア英語版 |
Hindley–Milner type system
In type theory and functional programming, Hindley–Milner (HM) (also known as Damas–Milner or Damas–Hindley–Milner) is a classical type system for the lambda calculus with parametric polymorphism, first described by J. Roger Hindley and later rediscovered by Robin Milner. Luis Damas contributed a close formal analysis and proof of the method in his PhD thesis.
Among HM's more notable properties is completeness and its ability to deduce the most general type of a given program without the need of any type annotations or other hints supplied by the programmer. Algorithm W is a fast algorithm, performing type inference in almost linear time with respect to the size of the source, making it practically usable to type large programs.〔Hindley–Milner is DEXPTIME-complete. However, non-linear behaviour only manifests itself on pathological inputs, as such the complexity theoretic proofs by and came as a surprise to the research community. When the depth of nested let-bindings is bounded—as is the case in realistic programs—Hindley–Milner type inference becomes polynomial.〕 HM is preferably used for functional languages. It was first implemented as part of the type system of the programming language ML. Since then, HM has been extended in various ways, most notably by constrained types as used in Haskell.
== Introduction ==
Organizing their original paper, Damas and Milner〔 clearly separated two very different tasks. One is to describe what types an expression can have and another to present an algorithm actually computing a type. Keeping the two aspects separate allows one to focus separately on the logic (i.e. meaning) behind the algorithm, as well as to establish a benchmark for the algorithm's properties.
How expressions and types fit to each other is described by means of a deductive system. Like any proof system, it allows different ways to come to a conclusion and since one and the same expression arguably might have different types, dissimilar conclusions about an expression are possible. Contrary to this, the type inference method itself (Algorithm W) is defined as a deterministic step-by-step procedure, leaving no choice what to do next. Thus clearly, decisions not present in the logic might have been made constructing the algorithm, which demand a closer look and justifications but would perhaps remain non-obvious without the above differentiation.
抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』
■ウィキペディアで「Hindley–Milner type system」の詳細全文を読む
スポンサード リンク
| 翻訳と辞書 : 翻訳のためのインターネットリソース |
Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.
|
|